\begin{tabbing}
es{-}first{-}at{-}since'(${\it es}$;$i$;$e$;$e$.$R$($e$);$e$.$P$($e$))
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=loc($e$) $=$ $i$\+
\\[0ex]\& $R$($e$)
\\[0ex]\& ($\exists$${\it e'}$:E. (${\it e'}$ $<$loc $e$) \& $P$(${\it e'}$) \& ($\forall$${\it e''}$:E. ${\it e'}$ $\leq$ ${\it e''}$  $\Rightarrow$ (${\it e''}$ $<$loc $e$) $\Rightarrow$ $\neg$$R$(${\it e''}$)))
\-
\end{tabbing}